
%{
  open Mods
  open Ast

  let mk_loc e l = { data = l; node = e }

  let loc e =
    mk_loc e (Parsing.symbol_start_pos (),Parsing.symbol_end_pos())

  let loc_i i e =
    mk_loc e (Parsing.rhs_start_pos i, Parsing.rhs_end_pos i)

  let loc_dummy e =
    mk_loc e (Lexing.dummy_pos, Lexing.dummy_pos)

  let cst = Hashtbl.create 32

  let rec eval_expr = function
    | Econst (c) -> c
    | Edesignator (d) ->
      begin match d.node with
        | DESid id -> Hashtbl.find cst id.node
        | _ -> failwith "Invalid designator for constant"
      end
    | Ebinop (op, e1, e2) ->
        let v1 = eval_expr e1.node in
        let v2 = eval_expr e2.node in
        begin match op with
          | Bplus -> Int32.add v1 v2
          | Bminus -> Int32.sub v1 v2
          | Bmul -> Int32.mul v1 v2
          | Bdiv -> Int32.div v1 v2
          | Bmod -> Int32.rem v1 v2
          | _ -> failwith "Invalid operator on constants" 
        end
    | _ -> failwith "Invalid constant expression"

  let parse_cst id e =
    let v = eval_expr e in
    Hashtbl.add cst id.node v

  let al2sm al =
    List.fold_left (fun a (id, t) -> StrMap.add id.node t a) StrMap.empty al

  let mk_desig d =
    match d.node with
    | DESid id -> begin try let v = Hashtbl.find cst id.node in
          Econst v
        with _ -> Edesignator d end
    | _ -> Edesignator d

%}

/* standard token */
%token          END PROGRAM PROCESS
%token          PROCEDURE ENDPROCEDURE FUNCTION ENDFUNCTION
%token          RULE ENDRULE RULESET ENDRULESET ALIAS ENDALIAS
%token          IF THEN ELSIF ELSE ENDIF SWITCH CASE ENDSWITCH
%token		FOR FORALL EXISTS IN DO ENDFOR ENDFORALL ENDEXISTS 
%token		WHILE ENDWHILE RETURN /* These added by rlm. */
%token		TO BEGIN BY /* added by rlm. */
%token		OLDEND /* for all the old types of END*. */
%token          LONGARROW DOTDOT ASSIGN CLEAR ERROR ASSERT PUT
%token          CONST TYPE VAR
%token          ENUM /* BOOLEAN */ INTERLEAVED RECORD ARRAY OF ENDRECORD /* BOOLEAN commented out because predefined enum */
/*%token		TRUE FALSE */ /* No need, it's a predefined enum */
%token          STARTSTATE ENDSTARTSTATE INVARIANT TRACEUNTIL
%token          LEQ NEQ	GEQ NOT IMPLIES /* ADDED */
%token		EOF DOT COMMA SC LCB RCB LSB RSB LP RP QM COL OR AND EQ LT GT PLUS MINUS TIMES DIV MOD /* ADDED*/
%token<string>  STRING
%token<string>	ID	/* was lex instead of string */
%token<int32> INTCONST

/* liveness token */
%token          FAIRNESS LIVENESS ALWAYS EVENTUALLY UNTIL FAILED UNFAIR
%token          LIVENESSSET ENDLIVENESSSET FAIRNESSSET ENDFAIRNESSSET

/* scalarset token */
%token          SCALARSET ISMEMBER 

/* "undefined" token */
%token          UNDEFINE ISUNDEFINED UNDEFINED

/* general union */
%token          UNION

/* multiset */
%token          MULTISET MULTISETREMOVE MULTISETREMOVEPRED MULTISETADD MULTISETCOUNT
%token          CHOOSE ENDCHOOSE

/* associativity */
%nonassoc	ASSIGN
%nonassoc	QM COL			/* C-style conditional. */
%nonassoc	IMPLIES			/* Boolean implication. */
%left		OR			/* boolean disjunction. */
%left 		AND			/* boolean conjunction. */
%left		NOT			/* Boolean negation. */
%nonassoc	LT LEQ EQ NEQ GEQ GT /* Comparisons. */
%left		PLUS MINUS		/* integer addition and subtraction. */
%left		TIMES DIV MOD		/* integer mult, div, and mod. */
					/* mod added by rlm. */

%start prog
%type <Ast.loc Ast.prog> prog

%%
/*************************************************************
 * The structure of this file is loosely a depth-first preorder
 * traversal of the tree of the grammar.
 */

/* The whole thing. */
prog:
| decls	procDecls rules EOF	{ (List.flatten (List.rev $1), [], $3) (* TODO *) }
;

/* general strongly-typed declarations. */
decls:
| /* empty */			{ [] }
| decls decl			{ $2::$1 } /* DAVID : ici erreur, il y avait $2::[] au lieu de $2::$1 */
;

/* A single declaration. */
decl:
| CONST constDecls		{ [] (*List.rev $2*) }
| TYPE typeDecls		{ List.rev $2 }
| VAR varDecls			{ List.flatten (List.rev $2) }
;

/* constant declarations. */
constDecls:
| /* empty */			{ (*[]*) }
| constDecls constDecl semi	{ (*$2::$1*) }
;

/* an optional semicolon. */
/* BUG:  please decide whether to have empty or not */
semi:
/*| /* empty			{ }*/
| SC				{ }
;

/* Identifier */
id:
| ID                            { loc $1 }
;

/* a single constant declaration. */
constDecl:
| id COL expr			{ parse_cst $1 $3.node (*; Dconst ($1, $3)*) }
;

/* type declarations. */
typeDecls:
| /* empty */			{ [] }
| typeDecls typeDecl semi	{ $2::$1 }
;

/* a single type declaration. */
typeDecl:
| id COL typeExpr		{ Dtype ($1, $3) }
;

/* a type expression, using the default $$ = $1 action. */
typeExpr:
| typeid			{ $1 } /* An already defined type. */
| enumtype			{ $1 }
| subrangetype			{ $1 }
| recordtype			{ $1 }
| arraytype			{ $1 }
| scalarsettype			{ $1 }
| uniontype			{ $1 }
| multisettype			{ $1 }
;

/* an already defined type. */
typeid:
| id				{ Tident $1 }
;

/* an enumerated type. */
enumtype:
| ENUM LCB enums RCB		{ Tenum $3 } /* should this be optenums? */
;

/* a possibly-empty comma-separated list. */
/*optenums:
| enums				{ (* UNUSED *) }
| /* empty *//*			{ (* UNUSED *) }
;*/

/* a comma-separated list of words. */
enums:
| enums COMMA id		{ $3::$1 }
| enums id			{ $2::$1 } /* invalid under Murphi2 */
| id				{ $1::[] }
;

/* a subrange of an enumerated type */
subrangetype:
| expr DOTDOT expr		{ Tsubrange (eval_expr $1.node, eval_expr $3.node) } /* must be constants. */
;

/* a record type, like the records of every Wirth language. */
recordtype:
| RECORD optInterleaved	fields endrecord	{ Trecord (al2sm (List.flatten $3)) }
;

/* End of a record. */
endrecord:
| ENDRECORD			{ }
| END				{ }
;

/* optional keyword INTERLEAVED. */
optInterleaved:
| /* empty */			{ (* FALSE *) }
/*| INTERLEAVED			{ (* TRUE *) }*/
;

/* a list of fields, with ; as a separator. */
fields:
| fields semi field		{ $3::$1 }
| fields semi			{ $1 }
| field				{ $1::[] }
;

/* a single field entry. */
field:
| id fieldtail			{ let idl, t = $2 in
				  let idl = $1::idl in
				  List.fold_left (fun accl id -> (id, t)::accl) [] idl
				}
;

/* end of a field--this is useful because it allows multiple fields
 * to be declared on a single line. */
fieldtail:
| COMMA id fieldtail		{ let idl, t = $3 in ($2::idl, t) }
| COL typeExpr			{ ([], $2) } /* the associated type. */
;

/* an array. */
arraytype:
| ARRAY optInterleaved LSB typeExpr RSB OF typeExpr 	{ Tarray ($4, $7) } /* $4 must be a simple type, not an array or record.*/
;

/* an multiset array. */
multisettype:
| MULTISET optInterleaved LSB expr RSB OF typeExpr	{ Tmultiset (eval_expr $4.node, $7) } /* $4 must be an integer, signifying the maximium size.*/
;

/* scalarset extension */
scalarsettype:
| SCALARSET LP expr RP		{ Tscalarset (eval_expr $3.node) } // a single scalarset
;

/* union extension */
uniontype:
| UNION LCB unionlist RCB	{ Tunion $3 } // a union of scalarsets and/or enum
;

unionlist:
| unionlist COMMA unionlistelt	{ $3::$1 }
| unionlistelt COMMA unionlistelt	{ $1::[$3] }
;

unionlistelt:
| id				{ Tident $1 }
| scalarsettype			{ $1 }
| enumtype			{ $1 }
;

/* var declarations. */
varDecls:
| /* empty */			{ [] }
| varDecls varDecl semi		{ $2::$1 }
;

/* a single var declaration. */
varDecl:
| id vardecltail		{ let idl, t = $2 in
				  let idl = $1::idl in
				  List.fold_left (fun accl id -> Dvar (id, t)::accl) [] idl
				}
;

/* end of a vardecl--this is useful because it allows multiple vars
 * to be declared on a single line. */
vardecltail:
| COMMA id vardecltail		{ let idl, t = $3 in ($2::idl, t) }
| COL typeExpr			{ ([], $2) } /* the associated type. */
;

/* a list of procedures. */
procDecls:
| /* empty */			{ [] (* TODO *) }
| procDecls procDecl		{ [] (* TODO *) }
| procDecls funcDecl		{ [] (* TODO *) }
;

/* a single procdure. */
procDecl:
| PROCEDURE id LP optformals RP semi optdecls optstmts endprocedure semi	{ (* TODO *) }	      
;

endprocedure:
| ENDPROCEDURE 			{ }
| END 				{ }
;

/* a single function. */
funcDecl:
| FUNCTION id LP optformals RP COL typeExpr semi optdecls optstmts endfunction semi	{ (* TODO *) }
;

endfunction:
| ENDFUNCTION 			{ }
| END 				{ }
;

/* an optional set of formals */
optformals:
| /* empty */ 			{ (* TODO *) }
| formals			{ (* TODO *) }
;

/* a nonempty list of formals */
formals:
| formals semi formal		{ (* TODO *) }
| formals semi			{ (* TODO *) }
| formal			{ (* TODO *) }
| formals COMMA formal		{ (* TODO *) }
;

/* a single formal. */
/* To add a type of parameter, you
 * must add a line that sets up paramclass correctly,
 * and add a case to the switch on paramclass in formaltail. */
formal:
| VAR formalrest		{ (* TODO *) }
| formalrest			{ (* TODO *) }
;

formalrest:
| id formaltail			{ (* TODO *) }
;

/* the end of a formal declaration. */
formaltail:
| COMMA id formaltail		{ (* TODO *) }
| COL typeExpr			{ (* TODO *) } /* was a TypeExpr, but I had to require param\'s types to be defined before. */
;

/* an optional declaration section and BEGIN keyword. */
optdecls:
| /* empty */			{ [] }
| decls BEGIN			{ List.flatten (List.rev $1) } /* DAVID : j'ai eu besoin de définir ça, j'espère que c'est correct */
;

/* expression syntax. */
/* a designator is an lvalue. */
designator:
| id				{ loc (DESid $1) }
| designator LSB expr RSB	{ loc (DESarray ($1, $3)) } /* array reference. */
| designator DOT id		{ loc (DESdot ($1, $3)) } /* record reference. */
;

/* general expression. */
expr:
| expr QM expr COL expr		{ loc (Econdition ($1, $3, $5)) }
| expr IMPLIES expr		{ loc (Ebinop (Bimplies, $1, $3)) }
| expr OR expr	 		{ loc (Ebinop (Bor, $1, $3)) }
| expr AND expr			{ loc (Ebinop (Band, $1, $3)) }
| NOT expr			{ loc (Enot $2) }
| expr LT expr			{ loc (Ebinop (Blt, $1, $3)) }
| expr LEQ expr			{ loc (Ebinop (Ble, $1, $3)) }
| expr GT expr			{ loc (Ebinop (Bgt, $1, $3)) }
| expr GEQ expr			{ loc (Ebinop (Bge, $1, $3)) }
| expr EQ expr			{ loc (Ebinop (Beq, $1, $3)) }
| expr NEQ expr			{ loc (Ebinop (Bne, $1, $3)) }
| expr PLUS expr		{ loc (Ebinop (Bplus, $1, $3)) }
| expr MINUS expr		{ loc (Ebinop (Bminus, $1, $3)) }
| PLUS expr	%prec TIMES	{ $2 }
| MINUS expr	%prec TIMES	{ loc (Ebinop (Bminus, loc (Econst 0l), $2)) } // DAVID : peut-être à adapter selon Econst
| expr TIMES expr		{ loc (Ebinop (Bmul, $1, $3)) }
| expr DIV expr			{ loc (Ebinop (Bdiv, $1, $3)) }
| expr MOD expr			{ loc (Ebinop (Bmod, $1, $3)) }
| INTCONST			{ loc (Econst $1) }
| designator			{ loc (mk_desig $1) }
| id actuals			{ loc (Efuncall ($1, $2)) } /* a function call. */
| ISUNDEFINED LP designator RP	{ loc (Eisundef $3) } // scalarset extension
| ISMEMBER LP designator COMMA typeExpr RP		{ loc (Eismem ($3, $5)) } // scalarset extension
| LP expr RP						{ $2 }
| FORALL quantifiers do_ expr endforall			{ loc (Eforall ($2, $4)) }
| EXISTS quantifiers do_ expr endexists			{ loc (Eexists ($2, $4)) }

    /* REMY : surement le meme error que tu as vu dans les rules
| error							{ $1 } */
        
| MULTISETCOUNT LP id COL designator COMMA expr RP	{ loc (Emultiset_count ($3, $5, $7)) } 	
;

     
endforall:
| ENDFORALL			{ }
| END				{ }
;

endexists:
| ENDEXISTS			{ }
| END				{ }
;

/* actual parameters for a function or procedure. */
actuals:
| LP exprlist RP		{ List.rev $2 }
| LP RP			{ [] }
;

/* a nonempty list of expressions. */
/* generated in reverse order. */
exprlist:
| exprlist COMMA expr		{ $3::$1 }
| expr				{ [$1] }
| exprlist COMMA UNDEFINED	{ $1 }
| UNDEFINED			{ [] }
;

/* the two types of FOR construct, marked off by braces in the following
 * examples:
 * 1) FOR {i := 1 to N BY 2} DO ...
 * 2) FOR {i : ind_t } DO ...
 */
quantifier:				/* DAVID : j'ai du définir ça pour que ça compile */
| id COL typeExpr		{ loc (Qvar ($1, $3)) }
| id ASSIGN expr TO expr optBy	{ loc (Qfor ($1, $3, $5, $6)) }
;

/* a semi-colon separated list of quantifiers. Only used for rulesets. */
quantifiers:
| quantifier SC quantifiers	{ $1::$3 }	/* DAVID : j'ai du définir ça pour que ça compile */
| quantifier			{ [$1] }
;

/* We've decided to try to let a colon substitute for the word 'do'. */
do_:
| DO				{ } 	
| COL				{ } 	
;

/* an optional BY phrase. */		/* DAVID : j'ai du définir ça pour que ça compile */
optBy:
| /* empty */			{ loc (Econst 1l) }
  /* DAVID : c'est l'incrément, plutôt que de mette un option, autant mettre 1 ici */
| BY expr			{ $2 }
;

/* statement rules. */
/* an optional list of statements. */
optstmts:
| /* empty */			{ [] }
| stmts				{ List.rev $1 }
  /* DAVID : j'ai mis [] juste pour que ça compile chez moi... */
    //REMY : ca me mache le travail *joke inside*
;

/* a list of statements, with ; as a separator. */
stmts:
| stmts semi stmt		{ $3::$1 }
| stmts semi			{ $1 } /* allow extra semi-colons. */
| stmt				{ [$1] }
;

/* a ;-separated statement. */
stmt:
| assignment			{ loc $1 }
| ifstmt			{ loc $1 }
| whilestmt			{ loc $1 }
| switchstmt			{ loc $1 }
| forstmt			{ loc $1 }
| proccall			{ loc $1 }
| clearstmt			{ loc $1 }
| errorstmt			{ loc $1 }
| assertstmt			{ loc $1 }
| putstmt 			{ loc $1 }
| aliasstmt 			{ loc $1 }
| returnstmt 			{ loc $1 }
| undefinestmt			{ loc $1 } // scalarset extension
| multisetaddstmt		{ loc $1 }
| multisetremovestmt		{ loc $1 }
;

/* an assignment statement. */
assignment:
| designator ASSIGN expr	{ Sassign ($1, $3) }
/* REMY : A mediter :  | designator ASSIGN UNDEFINED	{ Sassign  } // "undefined" extension */
;

/* if statement. */
ifstmt:
| IF expr THEN optstmts optElses endif	{ Sif ($2, $4, $5) }
;

endif:
| ENDIF				{ }
| END				{ }
;

/* elsif parts. */
optElses:
| elsif optElses		{ let e, stmts = $1 in [loc (Sif (e, stmts, $2))]  }
| optElse			{ $1 }
;

/* a single elsif. */
elsif:
| ELSIF expr THEN optstmts	{ ($2, $4) }
;

/* an optional else clause. */
optElse:
| /* empty */			{ [] }
| ELSE optstmts			{ $2 }
;

/* while statment. */
whilestmt:
| WHILE expr do_ optstmts endwhile	{ Swhile ($2, $4) }
;

endwhile:
| ENDWHILE			{ }
| END				{ }
;

/* switch statement. */
switchstmt:
| SWITCH expr optCases optElse endswitch	{ Sswitch ($2, $3, $4) }
;

endswitch:
| ENDSWITCH			{ }
| END				{ }
;

/* an optional list of cases. */
optCases:
| /* empty */			{ [] }
| optCases case			{ $2::$1 }
;

/* a single case. */
case:
| CASE exprlist COL optstmts	{ ($2, $4) }
;

/* for statement. */
forstmt:
| FOR quantifiers do_ optstmts endfor	{ Sfor ($2, $4) }
;

endfor:
| ENDFOR			{ }
| END				{ }
;

/* procedure call. */
proccall:
| id actuals			{ Sproccall ($1, $2) }
;

/* set all elements of basic type to their minima. */
clearstmt:
| CLEAR designator		{ Sclear $2}
;

/* undefine statement */
undefinestmt:
| UNDEFINE designator		{ Sundef $2 }
;

/* multiset add statement */
multisetaddstmt:
| MULTISETADD LP designator COMMA designator RP	{ Smultisetadd ($3, $5) }
;

/* multiset remove statement */
multisetremovestmt:
| MULTISETREMOVEPRED LP id COL designator COL expr RP { Smultisetremovepred ($3, $5, $7) }
| MULTISETREMOVE LP expr COMMA designator RP { Smultisetremove ($3, $5) }
;

/* raise an error. */
errorstmt:
| ERROR STRING			{ Serror $2 }
;

/* check an assertion, error if it's not so. */
assertstmt:
| ASSERT expr optString		{ Sassert ($2, $3) }
;

/* Print a message to output, I assume. */
putstmt:
| PUT expr			{ Sput (Putexpr $2) }
| PUT STRING			{ Sput (Putstring $2) }
;

/* simplify use of common expressions--sort of like a with statement. */
aliasstmt:
| ALIAS aliases do_ optstmts endalias	{ Salias ($2, $4) }
;

endalias:
| ENDALIAS			{ }
| END				{ }
;

/* a set of aliases. */		/* DAVID : j'ai eu besoin de définir ça pour avancer, c'est à vérifier */
aliases:
| aliases semi alias		{ $3::$1 }
| aliases semi			{ $1 }
| aliases COMMA alias		{ $3::$1 }
| alias				{ [$1] }
;

/* a single alias. */		/* DAVID : j'ai eu besoin de définir ça pour avancer, c'est à vérifier */
alias:
| id COL expr			{ ($1, $3) }
;

/* exit from a procedure, function or rule and return a value for a function */
returnstmt:
| RETURN optretexpr		{ Sreturn $2 }
;

/* an optional expression to be returned. */
optretexpr:
| /* empty */			{ None }
| expr				{ Some $1 }
;

/* Murphi-specific stuff. */
/* A list of rules to be applied nondeterministically. */
/* Okay, so it\'s right-recursive. Forgive me, please. */
rules:
| rule semi rules		{ $1::$3 }
| rule semi			{ $1::[] }
| rule				{ $1::[] }
;

/* a single rule--in essence, a hunk of code to execute nondeterministically.*/
/* Now, it could be a startstate or an invariant, too. rlm. */
rule:
| simplerule			{ loc $1 }
| aliasrule			{ loc $1 }
| ruleset			{ loc $1 }
| startstate			{ loc $1 }
| invariant			{ loc $1 }
//| fairness			{ (* UNUSED *) } // liveness extension
//| liveness			{ (* UNUSED *) } // liveness extension
//| error				{ (* perform magic--I don't understand this well. *) } /* DAVID : comment from Murphi source code... */
    //REMY : Epic
  // DAVID : I don't know how to manage the above production...
| choose			{ loc $1 }
;

/* a basic rule. */ 	/* DAVID : conflit shift/reduce sur optCondition, mais c'est mentionné dans la doc... */
simplerule:
| RULE /* optFair optPriority */ optString optCondition optdecls optstmts endrule { Rsimple ($2, $3, $4, $5) }
;

// liveness extension
optFair:
| /* empty */			{ (* FALSE *) }
| UNFAIR			{ (* TRUE *) }
;

endrule:
| ENDRULE			{ }
| END				{ }
;

/* an optional condition on a rule. */   
optCondition:
| /* empty */			{ loc (Econst 1l) } /* DAVID : plutôt que de mettre un option expr, autant mettre un 1, mais devrait être booléen ! */
| expr LONGARROW		{ $1 }
;

/* an optional name. */
optString:
| /* empty */			{ None }
  /* DAVID : voir si la chaîne vide est acceptable ici */
    //REMY : Mieux : un type option ocaml ;) 
| STRING			{ Some $1 }
/*| id				{ (* UNUSED *) }*/
;

/* Vitaly */

/* an optional priority */
optPriority:
| /* empty */			{ Econst 0l }
| INTCONST			{ Econst $1 }
;

/* an aliased ruleset. */
aliasrule:
| ALIAS aliases do_ rules endalias	{ Ralias ($2, $4) }
;
			  
/* a parametrized ruleset. */
ruleset:
| RULESET quantifiers do_ rules endruleset	{ Rruleset ($2, $4) }
;

endruleset:
| ENDRULESET			{ }
| END				{ }
;

/* choosing from a multiset */
choose:
| CHOOSE id COL designator do_ rules endchoose	{ Rchoose ($2, $4, $6) }
;

onerule:	/* DAVID : ca n'a pas l'air d'être utilisé, mais ça ne coute rien de le laisser */
| rule semi			{ $1 }
| rule				{ $1 }
;

endchoose:
| ENDCHOOSE			{ }
| END				{ }
;

/* a single start state. */
startstate:
| STARTSTATE optString optdecls optstmts endstartstate	{ Rstart ($2, $3, $4) }
;

endstartstate:
| ENDSTARTSTATE			{ }
| END				{ }
;

/* a list of invariants. */
/*optInvariants:
| /* empty *//*			{ (* UNUSED *) }
| optInvariants invariant	{ (* UNUSED *) }
;*/

/* a single invariant. */
invariant:
| INVARIANT optString expr	{ Rinvariant ($2, $3) }
;

/* a single fairness. */
fairness:
| FAIRNESS optString expr	{ (* UNUSED *) }
;

liveness:
| liveU				{ (* UNUSED *) }
| liveE				{ (* UNUSED *) }
| liveAE			{ (* UNUSED *) }
| liveEA			{ (* UNUSED *) }
| liveAIU			{ (* UNUSED *) }
| liveAIE			{ (* UNUSED *) }
;

liveU:
| LIVENESS optString expr UNTIL expr { (* UNUSED *) }
;

liveE:
| LIVENESS optString EVENTUALLY expr { (* UNUSED *) }
;

liveEA:
| LIVENESS optString EVENTUALLY ALWAYS expr { (* UNUSED *) }
;

liveAE:
| LIVENESS optString ALWAYS EVENTUALLY expr	{ (* UNUSED *) }
;

liveAIE:
| LIVENESS optString ALWAYS expr IMPLIES EVENTUALLY expr	{ (* UNUSED *) }
;

liveAIU:
| LIVENESS optString ALWAYS expr IMPLIES expr UNTIL expr	{ (* UNUSED *) }
;

